\newcommand{\jug}{\ensuremath{\mathcal{S}}}

We now proceed to investigate\done\todo[B35.]{Fixed, pls check.} \emph{safety} and \emph{consistency}, the main properties of our typing system.
While safety (discussed in \S\,\ref{ss:safety}) corresponds to the expected guarantee of adherence to prescribed session types and absence of runtime errors, 
consistency (discussed in \S\,\ref{ss:consist})  formalizes a correct interplay between communication actions and update actions.
Defining both properties requires the following notions of \emph{$\kappa$-processes}, \emph{$\kappa$-redexes}, 
and \emph{error process}.
These are classic ingredients in session types presentations (see, e.g., \cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07});
our notions generalize usual definitions 
to the case in which processes which may interact even if contained in arbitrarily nested transparent locations (formalized by the contexts of 
Def.~\ref{d:context}).

\begin{definition}[$\kappa$-processes, $\kappa$-redexes, errors]\label{d:kred}
A process $P$ is a \emph{$\kappa$-process} if it is a prefixed process with subject $\kappa$, i.e., 
$P$ is one of the following:
$$
%\begin{array}{llcllcrl}
%  &  \inC{\kappa^{\,p}}{\til{x}}.P' & &  & \outC{\kappa^{\,p}}{v}.P' & &    &  \close{\kappa^{\,p}}.P'  \\
%  &   \catch{\kappa^{\,p}}{x}.P' & &  &    \throw{\kappa^{\,p}}{d^{\,q}}.P' \\
%  &   \branch{\kappa^{\,p}}{n_1{:}P_1 \parallel \ldots \parallel n_m{:}P_m} ~~ & &  &   \select{\kappa^{\,p}}{n}.P' 
%\end{array}
\begin{array}{ll}
    \inC{\kappa^{\,p}}{\til{x}}.P' & \outC{\kappa^{\,p}}{v}.P'    \\
  \catch{\kappa^{\,p}}{x}.P' &  \throw{\kappa^{\,p}}{k^{\,q}}.P' \\
   \branch{\kappa^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}  &   \select{\kappa^{\,p}}{n}.P' \\
    \close{\kappa^{\,p}}.P' & 
\end{array}
$$
Process $P$ is a \emph{$\kappa$-redex} if 
it contains the composition of exactly two $\kappa$-processes with opposing polarities, i.e., 
for some contexts $C$, $D$ and $E$\done\todo[B36.]{Fixed, pls check}, and processes $P_1, P_2$, $P_m$, and $P'$, \done\todo[B15.]{I have changed this following the comment, please check.}
we have that 
$P$ is 
structurally congruent to
one of the following:
$$
\begin{array}{c}
(\nu \til{\kappa})(E\big\{C\{\inC{\kappa^{\,p}}{\til{x}}.P_1\} \para D\{\outC{\kappa^{\,\overline{p}}}{v}.P_2\}\big\}  )\\  
(\nu \til{\kappa})(E\big\{C\{\catch{\kappa^{\,p}}{x}.P_1\} \para  D\{\throw{\kappa^{\,\overline{p}}}{k^{\,q}}.P_2\} \big\}) \\
(\nu \til{\kappa})(E\big\{C\{\branch{\kappa^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \} \para  D\{  \select{\kappa^{\,\overline{p}}}{n_i};P'\}\big\} )  \\
(\nu \til{\kappa})(E\big\{C\{\close{\kappa^{\,p}}.P_1\}  \para  D\{\close{\kappa^{\,\overline{p}}}.P_2\}\big\})
\end{array}
$$
We say a $\kappa$-redex is \emph{located} if one or both of its $\kappa$-processes is inside at least one located process.

$P$ is an \emph{error} if
$P \equiv (\nu \til{\kappa})(Q \para R)$
where, for some $\kappa$, $Q$ contains 
\underline{either} 
%exactly one $\kappa$-process
%\underline{or}
exactly 
two $\kappa$-processes that do not form a $\kappa$-redex
\underline{or}
three or more $\kappa$-processes.
\end{definition}




\subsection{Session Safety}\label{ss:safety}


We now give
subject congruence and subject reduction results for our typing discipline.
Together with some 
some auxiliary results, these provide the basis for the proof of type safety (Theorem~\ref{t:safety} in Page~\pageref{t:safety}).
We start by giving three standard results, namely weakening, strengthening, and channel lemmas.


\begin{lemma}[Weakening]
 Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$.  If $\mathsf{X} \notin vdom(\Theta)$ then $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\INT'}}{P}{\type{\ActS}{\INT}}$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}


\begin{lemma}[Strengthening]
 Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$.
If $\mathsf{X}  \notin \mathsf{fv}(P)$ then $\judgebis{\env{\Gamma}{ \Theta \setminus \mathsf{X}:\INT'}}{P}{\type{\ActS}{\INT}}$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}



\begin{lemma}[Channel Lemma]\label{lem:channel}
  Let $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, 
 $\cha \notin \mathsf{fc}(P) \cup \mathsf{bc}(P)$ iff $\cha \notin dom(\ActS)$.
\end{lemma}
\begin{proof}
 Easily shown by induction on the structure of $P$.
\end{proof}

We are ready to show the Subject Congruence Theorem:

\begin{theorem}[Subject Congruence] \label{th:congr}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ and $P \equiv Q$ then $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}$.
\end{theorem}
\begin{proof}
By induction on the derivation of $P \equiv Q$, with a case analysis on the last applied rule. See~\ref{app:congr} for details.\done\todo[B17.]{We have moved the proof to the appendix.}
\end{proof}

The following auxiliary result concerns substitutions for channels, expressions, and process variables.
Observe how the case of process variables has been relaxed so as to allow substitution 
with a process with ``smaller'' interface (in the sense of \intpr, cf.  Not.~\ref{n:interf}). This extra flexibility is in line
with the typing rule for located processes (rule~\rulename{t:Loc}), and will be useful later on in proofs.
%In order to prove the subject reduction theorem we need some auxiliary results. The first lemma handles substitutions.

\begin{lemma}[Substitution Lemma]\label{lem:substitution}
\quad 
\begin{enumerate}
 \item \label{subchavar}If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS,x:\ST}{\INT}}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS, \cha^p:\ST }{\INT}}$ %\jp{This statement should be different, I think.} \todo{check if this new formulation" is what you were thinking} 
  \item \label{subvalvar}If $\judgebis{\env{\Gamma, \til{x}:\til{\tau}}{ \Theta}}{P}{\type{\ActS}{\INT}}$ and $\Gamma \vdash \til{e}:\til{\tau}$ then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\til{e}}{\til{x}}}{\type{\ActS}{\INT}}$. 
 % \item If $\judgebis{\env{\Gamma}{ \Theta}}{P}{\type{\ActS}{\INT}}$  then $\judgebis{\env{\Gamma}{ \Theta}}{P\sub{\cha^p}{x}}{\type{\ActS\sub{\cha^p}{x}}{\INT}}$. 
   \item \label{subprovar} If $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\INT}}{P}{\type{\emptyset}{\INT_1}}$ and $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\emptyset}{\INT'}}$ with $\INT' \intpr \INT$  then, for some $\INT'_1$, we have \\ 
   $\judgebis{\env{\Gamma}{\Theta}}{P\sub{Q}{\mathsf{X}}}{\type{\emptyset}{\INT'_1}}$ with $\INT'_1 \intpr \INT_1$. %\jp{in the proof, it'd be better to explain why this inequality holds}
\end{enumerate}
\end{lemma}
\begin{proof}
Easily shown by induction on the structure of $P$.
\end{proof}

 %Then, we need to introduce how to manipulate contexts, to this aim we define the 
 \done\todo[B18.]{Some comments on "type of contexts" do not longer apply, with typed contexts.}
 As reduction may occur inside contexts, in proofs it is useful to have \emph{typed contexts},
building upon Def.~\ref{d:context}. We thus have contexts in which the hole has associated typing information---concretely, the typing for processes which may fill in the hole. Defining context requires a simple extension of judgments, in the following way:
$$
\judgebis{\mathcal{H}; \env{\Gamma}{ \Theta}}{C}{\type{\ActS}{\INT}}
$$
Intuitively, $\mathcal{H}$ contains the description of the type associated to the hole in $C$.
Typing rules in Tables~\ref{tab:ts} and~\ref{tab:session}
are extended in the expected way.
Because contexts have a single hole, $\mathcal{H}$ is either empty of has exactly one element.
When $\mathcal{H}$ is empty,
we write $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}$ instead of
$\judgebis{\cdot \, ; \env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}$.
Two additional typing rules are required:
$$
\begin{array}{c}
\inferrule*[left=\rulename{t:Hole}] { }{\judgebis{\bullet_{\Gamma; \Theta \vdash \type{\ActS}{\INT}\,} ; \env{\Gamma}{\Theta}}{\bullet~}{\type{\ActS}{ \INT}}}		      
\\
\\
\inferrule*[left=\rulename{t:Fill}]		  
    {\judgebis{\bullet_{\Gamma; \Theta \vdash \type{\ActS}{\INT}\,} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1}{ \INT_1 }} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{ \INT }}} {\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_1}{ \INT_1}}}
\end{array}
$$
\noindent Axiom \rulename{t:Hole} allows us to introduce typed holes into contexts. 
In rule~\rulename{t:Fill}, $P$ is a process (it does not have any holes), and $C$ is a context with a hole of type $\Gamma; \Theta \vdash \type{\ActS}{ \INT}$. 
The substitution of occurrences of $\bullet$ in $C$ with $P$, noted $C\{P\}$ 
is sound as long as the typings of $P$ coincide with those declared in $\mathcal{H}$ for $C$.
Based on these  rules and Definitions~\ref{d:context} and~\ref{d:opcontx}, the following two auxiliary lemmas 
on properties of typed contexts follow easily. We first introduce some convenient notation for typed holes.

\begin{newnotation}
Let us use $\jug, \jug', \ldots$ to range over judgments
attached to typed holes. This way,
$\bullet_\jug$ denotes the valid typed hole associated to  $\jug = \Gamma; \Theta \vdash \type{\ActS}{\INT}$.
\end{newnotation}

%\begin{definition}[Type of contexts]
%Let $C$ be a context as in Def.~\ref{d:context}. 
%The type of $C$, denoted $\typecontx{C}{ \Gamma}{ \Theta}$, is 
%inductively defined as a pair:
%$$
%\begin{array}{ll}
% \typecontx{\bullet}{ \Gamma}{ \Theta} &= (\emptyset, \emptyset)\\
% \typecontx{\compo{l}{h}{C \para P}}{ \Gamma}{ \Theta}& = (\Pi_1( \typecontx{C}{\Gamma}{ \Theta}) \cup \ActS, ~\Pi_2(\typecontx{C}{\Gamma}{ \Theta}) \addelta \INT) \qquad \qquad \qquad \ \\
%  & \hfill \text{ if } ~\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}
%\end{array}
%$$
%where $\Pi_1(\typecontx{C}{ \Gamma}{ \Theta})$ 
%(resp. $\Pi_2(\typecontx{C}{ \Gamma}{ \Theta})$)
%denote the first (resp. second) element of pair 
%$\typecontx{C}{ \Gamma}{ \Theta}$.
%\end{definition}
%
%%\todo{Cambiare notazione $\typecontx{C}{ \Gamma}{\Theta}$}
%Next we state how to infer the type of a context:
%

A typed context may contain a typed hole in parallel with arbitrary behaviors.
This may have consequences on the typing and the interface, as 
the following lemma formalizes:

\begin{lemma}\label{lem:context}
 Let  $P$ and $C$ be a process and a typed context such that 
 $$\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS}{ \INT}}$$ is a derivable judgment.
 There exist $\ActS_1, \INT_1$ such that 
 (i) $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT}_1}$ is a well-typed process, and
 (ii) $\ActS_1 \subseteq \ActS$ and $\INT_1 \intpr \INT$.
\end{lemma}
%\begin{lemma}\label{lem:context} 
% $P$ be a process and $C$ a context as in Def.~\ref{d:context}. Then \\ $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{\INT_P}}$ and $\typecontx{C}{ \Gamma}{ \Theta} = (\ActS_C, \INT_C) $ iff 
%$\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_C \cup \ActS_P}{\INT_C \addelta \INT_P}}$
%\end{lemma}
%\begin{proof}
%By induction on the structure of the context $C\{\bullet\}$. The proof for the $(\Rightarrow)$ directions follows by observing that the only rules applied for typing $C\{P\}$ are  \rulename{t:Loc} and \rulename{t:Par} that either do not  change or can  only extend $\ActS_P$ and $\INT_P$. The opposite direction $(\Leftarrow)$, similarly, relies on the typing inversion on the same rules
% \rulename{t:Loc} and \rulename{t:Par}.
%\end{proof}
%%
%
%\begin{newnotation}
%In the proof of Theorem~\ref{th:subred}, we shall use the following notation 
%to denote an use of  Lemma \ref{lem:context}:
%$$
%\infer={\judgebis{\env{\Gamma}{\Theta}}{C\{P\}}{\type{\ActS_P, \ActS_C}{ \INT_P \uplus \INT_C}}}		  
%    {\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_P}{ \INT_P }}}
%$$
%\end{newnotation}




%\jp{Now I tend to think that we may need something like Lemma \ref{lem:context}. 
%The point is that in the proof we would like to get rid of contexts, justifying the ellipses (not to enclose processes within contexts, as Lemma 9 does). 
%With such a lemma, we could "go up" in the typing tree until we have something without contexts.
%At that point, we apply something (say, a substitution lemma). Then, we conclude by "going down" again, reconstructing the context. The proof would be indeed by structural induction on the context (base case: empty contexts--trivial; cases for locations/restriction are easy by IH and typing inversion).}

%\jp{Why not writing this as a corollary?}
%\todo{Maybe just a remark}
% Notice that previous lemma allows us to conclude that, given a process $P$ and a context $C$, if $\judgement{\Gamma}{\Theta}{C[P]}{\ActS}{\INT}$ then there exists $\Gamma, \Theta, \ActS', \INT'$ such that $\judgement{\Gamma}{\Theta}{P}{\ActS'}{\INT'}$.


%\todo{Subject reduction works for balanced environments; we need to introduce that notion. }

The following property formalizes the effect that a type hole has in the typing judgment of a context:
under certain conditions, 
if the typing and interface of the hole change, then the judgment for the whole context should change as well.

\begin{lemma}\label{l:ctxop}
Let $C$ be a context as in Def.~\ref{d:context}. %Then we have:
\begin{enumerate}[1.]
\item 
Suppose
$\judgebis{\bullet_\jug ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1,k_2:\STT,\ActS'}{ \INT_1 \addelta \INT_2 \addelta \INT'}}$ 
with  $\jug = {\Gamma; \Theta \vdash \type{\ActS_1,k_2:\STT}{\INT_1 \addelta \INT_2}}$
is well-typed. 
Let  $\jug' = {\Gamma; \Theta \vdash \type{\ActS_1, k_1:\ST,k_2:\STT'}{\INT_1}}$.
Then
$$\judgebis{\bullet_{\jug'} ; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS_1, k_1:\ST, k_2:\STT', \ActS'}{ \INT_1 \addelta \INT'}}$$
is a derivable judgment.

\item Suppose $\judgebis{\bullet_{\jug} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1, k_1{:}\ST, k_2{:}\STT, \ActS'}{ \INT_1 \addelta \INT_2 \addelta \INT' }}$ with $\jug = {\Gamma; \Theta \vdash \type{\ActS_1, k{:}\ST, k_2{:}\STT}{\INT_1 \addelta \INT_2}}$
is well-typed. 
%with $\jug = {\Gamma; \Theta \vdash \type{\ActS_1, k{:}\ST, k_2{:}\STT}{\INT_1 \addelta \INT_2}}$
Let $\jug' = {\Gamma; \Theta \vdash \type{\ActS_1, k_2{:}\STT'}{\INT_1}}$.
Then %the judgment
$$\judgebis{\bullet_{\jug'} ; \env{\Gamma}{\Theta}}{C^-}{\type{\ActS_1, k_2{:}\STT', \ActS}{ \INT_1 \addelta \INT' }}$$
is a derivable judgment.

\item Suppose $\judgebis{\bullet_{\jug} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_C \cup \ActS_{\jug}}{ \INT_C \addelta \INT_{\jug} }}$ with $\jug = {\Gamma; \Theta \vdash \type{\ActS_{\jug}}{\INT_{\jug}}}$
is well-typed. 
Let $\jug' = {\Gamma; \Theta \vdash \type{\ActS_{\jug'}}{\INT_{\jug'}}}$.
Then 
$$\judgebis{\bullet_{\jug'} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_C \cup \ActS_{\jug'}}{ \INT_C \addelta \INT_{\jug'} }}$$
is a derivable judgment.
\end{enumerate}
The analogous of (1) and (2), involving 
%%Cases when the type of the hole refers to 
bracketed assignments, are as expected.
\end{lemma}

We now introduce the usual notion of \emph{balanced typing}~\cite{DBLP:journals/entcs/YoshidaV07}:

\begin{definition}[Balanced Typings]\label{d:balanced}
We say a typing 
$\ActS$ is \emph{balanced} iff 
for all $\kappa^p:\ST \in \ActS$ (resp. $[\kappa^p:\ST] \in \ActS$)
then also 
$\kappa^{\overline{p}}: \overline{\ST} \in \ActS$ (resp. $[\kappa^{\overline{p}}: \overline{\ST}] \in \ActS$).
%for all $\kappa^p:\ST \in \ActS$ then also 
%$\kappa^{\overline{p}}: \overline{\ST} \in \ActS$, and 
%for all $[\kappa^p:\ST] \in \ActS$ then also
%$[\kappa^{\overline{p}}: \overline{\ST}] \in \ActS$.
\end{definition}

The final requirement for proving safety via typing is the subject reduction theorem below.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{theorem}
\begin{proof}
%%The proof proceeds by 
By induction on the last rule applied in the reduction. See~\ref{app:subred} for details.
\end{proof}

%\begin{proof}
%%The proof proceeds by 
%By induction on the last rule applied in the reduction. See~\ref{app:subred} for details. 
%We assume that $\til{e} \downarrow \til{c}$ is a type preserving operation, for every $\til{e}$.
%\todo[B19.]{Write a short proof sketch, as suggested?}
%%\begin{description}
%\paragraph{\bf Case \rulename{r:Open}} From Table~\ref{tab:semantics} we have:
%\begin{multline*} 
%E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} \pired  \\
%E^{++}_{} \big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }\big)\big\} } 
%\end{multline*}
%By assumption  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\} }{\type{\ActS}{\INT}}$
%with balanced $\ActS$.
%Then, by %the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) three times,  and  
%inversion on typing, using rules \rulename{t:Fill}, \rulename{t:Accept}, \rulename{t:Request}, and \rulename{t:Par} we infer
%there exist $\ActS', \INT'$ such that
%{%\small
%\begin{equation}\label{eq:wholeopen}
%\infer
%{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}\big\}}{\type{\ActS}{\INT }}}
%{
%\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}   & 	\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_{2}\}}{\type{\ActS'}{\INT'}}}
%{    \eqref{eq:typeaccept} & \eqref{eq:typerequest}
%}}
%\end{equation}
%}
%where
%$ \INT' = (\INT'_1 \addelta a:\ST_\qual) \addelta (\INT'_2\addelta a:\overline{\ST}_\qual )$
%%$\{ a:\ST_\qual \addelta a:\overline{\ST}_\qual \} \subseteq \INT$, 
%and
%\begin{equation}
%\jug_0 = \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjug0}
%\end{equation}
%%Moreover,
%By Lemma~\ref{lem:context},  
%$\ActS' \subseteq \ActS$ and $\INT' \intpr \INT$.
%Then, letting $\ActS' = \ActS'_1 \cup \ActS'_2$, 
%subtree \eqref{eq:typeaccept} is as follows: %\todo[JP:]{We should explain why $\ActS$ is different from $\ActS'$}:
%\begin{equation}\label{eq:typeaccept}
%\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\nopena{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta a:\ST_\qual }}}		  
%    { 
% 	\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1\addelta a:\ST_\qual}} & \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopena{a}{x}.P_1}{\type{\ActS_1}{ \INT_1\addelta a:\ST_\qual  }}}
%  {\Gamma \vdash a: \langle \ST_\qual , \overline{\ST}_\qual \rangle &
%\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, x:\ST}{\INT_1}} }}
%\end{equation}
%with 
%\begin{equation}
%\jug_1 = \Gamma; \Theta \vdash \type{\ActS_1}{\INT_1 \addelta a:\ST_\qual} \label{eq:srjug1}
%\end{equation}
%Then, subtree~\eqref{eq:typerequest} is as follows:
%\begin{equation}\label{eq:typerequest}
%\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_{2} \}}{ \type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual }}}
%	{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual}} &  \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_{2}}{ \type{\ActS_2}{ \INT_2\addelta a:\overline{\ST}_\qual }}}
%	{\Gamma \vdash a: \langle \ST_\qual , \overline{\ST}_\qual \rangle &
%\judgebis{\env{\Gamma}{\Theta}}{P_{2}}{\type{\ActS_2, y:\overline{\ST}}{\INT_2}}}
%}
% \end{equation}
% with 
% \begin{equation}
% \jug_2 = \Gamma; \Theta \vdash \type{\ActS_2}{\INT_2 \addelta a:\overline{\ST}_\qual} \label{eq:srjug2}
% \end{equation}
%By Lemma~\ref{lem:context} 
%% ($\Leftarrow$) 
%%there exist $\ActS_1, \ActS_2$ such that 
%we have that 
%$\ActS_1 \subseteq \ActS_1'$ and $\ActS_2 \subseteq \ActS_2'$. We also infer $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, and $\INT' \intpr \INT$. 
% Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on judgments for $P_1$ and $P_2$, we obtain:
% \begin{enumerate}[(a)]
% \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}$.
% \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
% \end{enumerate}
%%By using Lemma \ref{lem:context}($\Rightarrow$)  and typing rules \rulename{t:Par} and \rulename{t:CRes} 
%We now describe how to obtain appropriately typed contexts $C^+, D^+$, and $E^{++}$ based on the information inferred up to here
%on contexts $C, D$, and $E$.
%%We give details for the case of $C^+$; cases for $D^+$ and $E^{++}$ follow analogously. 
%We first describe the case of $C^+$.
%From \eqref{eq:typeaccept} above we obtained
%$\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 \addelta a:\ST_{\qual}}}$
%with $\jug_1$ as in \eqref{eq:srjug1}.
%Then, using Lemma~\ref{l:ctxop}(1), we infer
%$\judgebis{\bullet_{\jug_3}; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST}{ \INT'_1}}$
%with 
% \begin{equation}
% \jug_3 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^+:\ST}{\INT_1} \label{eq:srjug3}
% \end{equation}
%We may now reconstruct the derivation given in \eqref{eq:typeaccept}:
%%$$R \triangleq {{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }},$$
%\begin{equation}\label{eq:typeacceptsub}
%\infer{\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{P_{1}\sub{\cha^+}{x}\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' }}}		  
%    { \judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST\,}{ \INT'_1}} &  
%    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x}}{ \type{\ActS_1, \cha^+:\ST}{\INT_1}}}
%\end{equation}
%For $D^+$, we proceed analogously from \eqref{eq:typerequest} and infer:
%\begin{equation}\label{eq:typerequestsub}
% \infer{\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_{2}\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
%	{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^-:\overline{\ST}}{ \INT'_2}} & \judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
%\end{equation}
%with 
% \begin{equation}
% \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^-:\overline{\ST}}{\INT_2} \label{eq:srjug4}
% \end{equation}
%To infer the type of $E^{++}$ we proceed as before using twice Lemma~\ref{l:ctxop}(1), combined with~\eqref{eq:srjug0}.
%We may finally derive the type for the result of the reduction: using rules \rulename{t:Par}, \rulename{t:CRes}, and \rulename{t:Fill} we obtain:
%$$
%\infer
%{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{} \big\{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}} \big\} }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT''}}}
%{(\ref{eq:last})   &
%	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \addelta \INT_2'}}}
%{\infer{\judgebis{\env{\Gamma}{\Theta}}{{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}{
%(\ref{eq:typeacceptsub})
%%
%&
%%
%	(\ref{eq:typerequestsub})
%}
%}}
%$$
%with 
% \begin{equation}\label{eq:last}
%\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{ \INT'' }}
% \end{equation}
%and 
%$$
% \jug_5 =  \Gamma; \Theta \vdash \type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'}
%$$
%
%Notice that by Lemma \ref{lem:context}, we have $\INT'' \intpr \INT_1' \cup \INT_2'$.
%Also, observe that by assumption $\ActS$ is balanced; therefore, 
%by Def.~\ref{d:balanced}
%the resulting typing $\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]$ is balanced too.
%This concludes this case. \done\todo[C18.]{The resulting typing is balanced by assumption, because we are adding two complementary entries, thus preserving balanced typing.}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%\paragraph{\bf Case \rulename{r:ROpen}} From Table~\ref{tab:semantics} we have: 
%\begin{multline*}
%          E\big\{C\{\repopen{a}{x}.P_1\}  \para  D\{\nopenr{a}{y}.P_2\} \big\}  \pired  \\
%E^{++}_{}\big\{\restr{\cha}{\big({C^{+}_{}\{P_1\sub{\cha^+}{x}  \para \repopen{a}{x}.P_1 \}  \para  D^{+}_{}\{P_2\sub{\cha^-}{y}\} }\big)}\big\}  
%         \end{multline*}
%
%\noindent By assumption $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\} }{\type{\ActS}{\INT}}$, with balanced $\ActS$.  
%Then, by inversion on typing, using rules
%%is obtained by the following derivation tree using Lemma \ref{lem:context}($\Leftarrow$) three times and inversion on  rules 
%\rulename{t:Fill}, 
%\rulename{t:RepAccept}, \rulename{t:Request}, and \rulename{t:Par}, we infer there exist $\ActS'$, $\INT'$ such that:
%$$
%\infer
%{ \judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}\big\}}{\type{\ActS}{\INT}}}
%{ \judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\} \para  D\{\nopenr{a}{y}.P_2\}}{\type{\ActS'}{\INT'}}}
%{
%\eqref{eq:bangaccept}
%%
%&
%%
%\eqref{eq:bangrequest}
%}}
%$$
%where
%$ \INT' = (\INT'_1 \addelta a:\ST_\quau) \addelta (\INT'_2\addelta a:\overline{\ST}_\qual )$
%%$\{ a:\ST_\qual \addelta a:\overline{\ST}_\qual \} \subseteq \INT$, 
%and
%\begin{equation}
%\jug_0 = \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjugro0}
%\end{equation}
%By Lemma~\ref{lem:context},  
%$\ActS' \subseteq \ActS$ and $\INT' \intpr \INT$.
%Then, letting $\ActS' = \ActS'_1 \cup \ActS'_2$, 
%subtree \eqref{eq:bangaccept} is as follows:
%%where (\ref{}) and (\ref{eq:bangrequest}) correspond to the subtrees:
%\begin{equation}\label{eq:bangaccept}
%	\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\repopen{a}{x}.P_1\}}{\type{\ActS_1'}{ \INT_1'\addelta a:\ST_\quau }}}		  
%    { \judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1\addelta a:\ST_\quau}} & 
%    	\infer{\judgebis{\env{\Gamma}{\Theta}}{\repopen{a}{x}.P_1}{\type{\emptyset}{\,\unres(\INT_1)\addelta a:\ST_\quau }}}
%  {\Gamma \vdash a: \langle \ST_\quau , \overline{\ST }_\qual \rangle &
%\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{x:\ST}{\INT_1}} }}
%\end{equation}
%with 
%\begin{equation}
%\jug_1 = \Gamma; \Theta \vdash \type{\emptyset}{\,\unres(\INT_1)\addelta a:\ST_\quau} \label{eq:srjugro1}
%\end{equation}
%Then, subtree \eqref{eq:bangrequest} is as follows:
%
%\begin{equation}\label{eq:bangrequest}
% \infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nopenr{a}{y}.P_2 \}}{ \type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_{\qual} }}}
%	{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2\addelta a:\overline{\ST}_\qual}}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{\nopenr{a}{y}.P_2}{ \type{\ActS_2}{ \INT_2\addelta a:\overline{\ST}_{\qual} }}}
%	{\Gamma \vdash a: \langle \ST_\quau , \overline{\ST}_\qual \rangle &
%\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS_2, y:\overline{\ST }}{\INT_2}}}
%}
%\end{equation}
% with 
% \begin{equation}
% \jug_2 = \Gamma; \Theta \vdash \type{\ActS_2}{\INT_2 \addelta a:\overline{\ST}_\qual} \label{eq:srjugro2}
% \end{equation}
%\noindent %where\done\todo[B37.]{Fixed, pls check} 
%By Lemma~\ref{lem:context} we have  
%$\ActS_1 \subseteq \ActS'_1$ and
%$\ActS_2 \subseteq \ActS_2'$. Moreover, $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$ and $\INT' \intpr \INT$.
%% where $ \INT' = (\INT'_1 \addelta \inter{a}{\ST}{\infty}) \addelta (\INT'_2\addelta \inter{a}{\overline{\ST}}{1} )$. 
% Now, using Lemma~\ref{lem:substitution}(\ref{subchavar}) on $P_1$ and $P_2$, we have:
% \begin{enumerate}[(a)]
% \item $\judgebis{\env{\Gamma}{ \Theta}}{P_1\sub{\cha^+}{x}}{ \type{ \cha^+:\ST}{\INT_1}}$.
% \item $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}$.
% \end{enumerate}
% We now describe how to obtain appropriately typed contexts $C^+, D^+$, and $E^{++}$ based on the information inferred up to here
%on contexts $C, D$, and $E$. We first describe the case of $C^+$.
%From~\eqref{eq:bangaccept} above we obtained
%$\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 \addelta a:\ST_{\quau}}}$
%with $\jug_1$ as in \eqref{eq:srjugro1}.
% Then, using Lemma~\ref{l:ctxop}(1), we infer
%$\judgebis{\bullet_{\jug_3}; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST}{ \INT'_1}}$
%with 
% \begin{equation}
% \jug_3 =  \Gamma; \Theta \vdash \type{\cha^+:\ST}{\unres(\INT_1)\addelta a:\ST_\quau} \label{eq:srjugro3}
% \end{equation}
%We may now reconstruct the derivation given in \eqref{eq:bangaccept}:
%\begin{equation}\label{eq:bangacceptsubfin}
%\infer{\judgebis{\env{\Gamma}{\Theta}}{C^{+}\{P_{1}\sub{\cha^+}{x}\}}{\type{\ActS_1', \cha^+:\ST}{ \INT_1' \addelta a:\ST_\quau}}}		  
%    { \judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^+}{\type{\ActS'_1, \cha^+:\ST\,}{ \INT'_1 \addelta a:\ST_\quau}} &  
%    	\judgebis{\env{\Gamma}{ \Theta}}{P_{1}\sub{\cha^+}{x}}{ \type{ \cha^+:\ST}{\unres(\INT_1)\addelta a:\ST_\quau}}}
%\end{equation}
%For $D^+$, we proceed analogously from \eqref{eq:bangrequest} and infer:
%\begin{equation}\label{eq:bangrequestsubfin}
% \infer{\judgebis{\env{\Gamma}{\Theta}}{D^{+}\{P_{2}\sub{\cha^-}{y}\}}{\type{\ActS'_2,\cha^- :\overline{\ST } }{\INT'_2}}}
%	{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^-:\overline{\ST}}{ \INT'_2}} & \judgebis{\env{\Gamma}{ \Theta}}{P_{2}\sub{\cha^-}{y}}{\type{\ActS_2,\cha^- :\overline{\ST } }{\INT_2}}}
%\end{equation}
%with 
% \begin{equation}
% \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^-:\overline{\ST}}{\INT_2} \label{eq:srjugro4}
% \end{equation}
%To infer the type of $E^{++}$ we proceed as before using twice Lemma~\ref{l:ctxop}(1), combined with~\eqref{eq:srjugro0}.
%We may finally derive the type for the result of the reduction: using rules \rulename{t:Par}, \rulename{t:CRes}, and \rulename{t:Fill} we obtain:
%$$
%\infer
%{\judgebis{\env{\Gamma}{\Theta}}{E^{++}_{} \big\{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}} \big\} }{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT''}}}
%{(\ref{eq:banglast})   &
%	\infer{\judgebis{\env{\Gamma}{\Theta}}{\restr{\cha}{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\}}}{\type{\ActS', [\cha^+:\ST], [\cha^-:\overline{\ST}]}{\INT_1' \addelta \INT_2'\addelta a:\ST_\quau}}}
%{\infer{\judgebis{\env{\Gamma}{\Theta}}{{C^{+}_{}\{P_{1}\sub{\cha^+}{x}\}  \para  D^{+}_{}\{P_{2}\sub{\cha^-}{y}\} }}{\type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'\addelta a:\ST_\quau}}}{
%\eqref{eq:bangacceptsubfin}
%%
%&
%%
%	\eqref{eq:bangrequestsubfin}
%}
%}}
%$$
%with 
% \begin{equation}\label{eq:banglast}
%\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]}{ \INT'' }}
% \end{equation}
%and 
%$$
% \jug_5 =  \Gamma; \Theta \vdash \type{\ActS', \cha^+:\ST, \cha^-:\overline{\ST} }{ \INT_1' \addelta \INT_2'\addelta a:\ST_\quau}
%$$
%Notice that by Lemma \ref{lem:context}, we have $\INT'' \intpr \INT_1' \cup \INT_2'\addelta a:\ST_\quau$.
%Also, observe that by assumption $\ActS$ is balanced; therefore, 
%by Def.~\ref{d:balanced}
%the resulting typing $\ActS, [\cha^+:\ST], [\cha^-:\overline{\ST}]$ is balanced too.
%This concludes this case. \done\todo[C18.]{The resulting typing is balanced by assumption, because we are adding two complementary entries, thus preserving balanced typing.}
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%\paragraph{\bf Case \rulename{r:Upd}} From Table~\ref{tab:semantics} we have:
%$$E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\} 
%\pired   
%E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$$
%By assumption we have $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\}}{ \type{\ActS}{\INT}}$,
%with $\ActS$ balanced.
%Then, by inversion on typing, using rules
%%is obtained by the following derivation tree using Lemma \ref{lem:context} ($\Leftarrow$) and  inversion on rules 
%\rulename{t:Fill}, \rulename{t:Par}, \rulename{t:Adapt}, and \rulename{t:Loc} we infer:
%\begin{equation}\label{eq:srupd00}
%\infer
%{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}\big\}}{ \type{\ActS}{\INT}}}
%{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{ \INT }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} \para  D\{\adapt{l}{P_2}{\mathsf{X}}\}}{ \type{\ActS'}{\INT'}}}
%{
%\eqref{eq:srupd0}
%&
%\eqref{eq:srupd1}
%}}
%\end{equation}
%with
%$\jug_0 =  \Gamma; \Theta \vdash \type{\ActS'}{\INT'}$.
%By Lemma~\ref{lem:context}, we have
%$\ActS' \subseteq \ActS'$ and $\INT' \intpr \INT$.
%Moreover, 
%letting $\ActS' = \ActS'_1 \cup \ActS'_2$ and $\INT' = \INT'_1 \addelta \INT'_2$, 
%subtree \eqref{eq:srupd0} is as follows:
%\begin{equation}\label{eq:srupd0}
%\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\component{l}{0}{}{P_1}\} }{ \type{\ActS'_1}{\INT'_1}}}
%{\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1}{ \INT'_1 }}  & \infer{\judgebis{\env{\Gamma}{\Theta}}{\compo{l}{0}{P_1}}{ \type{\emptyset}{\INT''_1}}}
%{ \INT''_1 \intpr \INT^*_1 & \Theta \vdash l:\INT^*_1
%  & \judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\emptyset}{\INT''_1} }   }}
%\end{equation}
%with
%$\jug_1 =  \Gamma; \Theta \vdash \type{\emptyset}{\INT''_1}$,
%and $\INT''_1 \intpr \INT'_1$ (by Lemma~\ref{lem:context}).
%Subtree \eqref{eq:srupd1} is as follows:
%\begin{equation}\label{eq:srupd1}
%\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\adapt{l}{P_2}{\mathsf{X}}\}}{ \type{\ActS'_2}{\INT'_2}}}{
%\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2}{ \INT'_2 }} & 
%\infer{\judgebis{\env{\Gamma}{\Theta}}{ \adapt{l}{P_2}{\mathsf{X}}}{ \type{\emptyset}{\emptyset}}}
%{\Theta \vdash l:\INT^*_1  &  \judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\INT^*_1}}}{P_2}{\type{\emptyset}{ \INT_3 }}}}
%\end{equation}
%with
%$\jug_2 =  \Gamma; \Theta \vdash \type{\emptyset}{\emptyset}$.
%%By Lemma \ref{lem:context} ($\Leftarrow$) we have $\ActS_1 \cup \ActS_2 \subseteq \ActS$, $\INT_2 \intpr \INT_2'$, $\INT_4 \intpr \INT_4'$, and $\INT_2' \addelta \INT_4' \intpr \INT$. 
%By Lemma~\ref{lem:substitution}(\ref{subprovar}) we have  $\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}$,
%for some $\INT'_3$ such that $\INT'_3 \intpr \INT_3$.
%We now reconstruct the derivation in \eqref{eq:srupd00}, using rules
%\rulename{t:Par}, \rulename{t:Fill} and Lemma~\ref{l:ctxop}(3). Let
%%, thus process $E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}$ can be typed by means of Lemma~\ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}:
%\begin{equation}\label{eq:finupd}
%\infer
%{\judgebis{\env{\Gamma}{\Theta}}{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}}{ \type{\ActS'_1 \cup \ActS'_2}{\INT''_3 \addelta \INT_2'}}}
%{\infer{\judgebis{\env{\Gamma}{\Theta}}{ C\{P_2\sub{P_1}{\mathsf{X}}\} }{\type{\ActS'_1}{\INT''_3}}}{
%\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1'}{ \INT_3'' }} &
%\judgebis{\env{\Gamma}{\Theta}}{ P_2\sub{P_1}{\mathsf{X}}}{\type{\emptyset}{\INT'_3}}}
%&
%\infer{\judgebis{\env{\Gamma}{\Theta}}{D\{\nil\}}{ \type{\ActS'_2}{\INT'_2}}}{
%\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2'}{ \INT_2' }}
%&\judgebis{\env{\Gamma}{\Theta}}{\nil}{ \type{\emptyset}{\emptyset}}}
%}
%\end{equation}
%and
%$$
%\infer{\judgebis{\env{\Gamma}{\Theta}}{E_{}\big\{C\{P_2\sub{P_1}{\mathsf{X}}\}  \para  D\{\nil\}\big\}}{ \type{\ActS}{\INT'}}}
%{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT'}}
%&(\ref{eq:finupd})}
%$$
%with
%$$
%\begin{array}{c}
%\jug_5 =  \Gamma; \Theta \vdash \type{\ActS'_1 \cup \ActS'_2}{\INT''_3 \addelta \INT'_2}
% \end{array}
%$$
%where by Lemma \ref{lem:context} %($\Rightarrow$) 
%we know $\INT_3'' \intpr \INT'_3$ and $\INT_3'' \addelta \INT_2' \intpr \INT'$.
%This concludes the analysis for this case.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%\paragraph{\bf Case \rulename{r:I/O}} From Table~\ref{tab:semantics} we have:
%$$E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} 
%\pired 
%E\big\{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}\big\} \quad (\til{e} \downarrow \til{c})$$
%By assumption, we have $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} }{ \type{\ActS}{\INT}}$, with $\ActS$ balanced.
%By inversion on typing, using rules 
%%we obtain the following derivation that employs Lemma~\ref{lem:context} ($\Leftarrow$) three times and inversion on rules  
%\rulename{t:Fill}, \rulename{t:Par}, \rulename{t:In}, and \rulename{t:Out}, we infer:
%%$$
%%R \triangleq C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}
%%$$
%$$
%\infer{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}\big\} }{ \type{\ActS}{\INT}}}
%{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT}} & \infer
%{
%\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{\,p}}{\til{e}}.P_1\} \para  D\{\inC{\cha^{\,\overline{p}}}{\til{x}}.P_2\}} {\type{\ActS'}{ \INT_1' \addelta \INT_2'}}}
%{ \eqref{eq:out}
%&
%\eqref{eq:in}
%}}
%$$
%where:
%\begin{eqnarray}
%\ActS' & = & \ActS_1' \cup \ActS_2', \cha^p:!(\til{\capab}).{\ST}, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST} \\
%\INT & = & \INT_1' \addelta \INT_2' \\
%\jug_0 & = &   \Gamma; \Theta \vdash \type{\ActS'}{\INT'_1 \addelta \INT'_2}
%\end{eqnarray}
%Moreover, by Lemma~\ref{lem:context}, we infer $\ActS' \subseteq \ActS$ and $\INT'_1 \addelta \INT'_2 \intpr \INT$.
%Also, we have that subtree (\ref{eq:out}) 
%is as follows:
%\begin{equation}\label{eq:out} 
%\infer{\judgebis{\env{\Gamma}{\Theta}}{C\{\outC{\cha^{p}}{\til{e}}.P_1\} } {\type{\ActS_1',  \cha^p:!(\til{\capab}).{\ST} }{ \INT_1' }}}{
%\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS_1}{ \INT'_2 }} &   \infer
%{\judgebis{\env{\Gamma}{\Theta}}{\outC{\cha^p}{\til{e}}.P_1}{\type{\ActS_1, \cha^p:!(\til{\capab}).{\ST}}{ \INT_1}}}
%{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS_1, \cha^p:{\ST}}{ \INT_1}} & \Gamma \vdash \til{e}:\til{\capab}}}
%\end{equation}
%with
%$$
% \jug_1 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^p:!(\til{\capab}).{\ST}}{ \INT_1}
%$$
%Also, subtree (\ref{eq:in}) is as follows:
%\begin{equation}\label{eq:in}
% \infer{\judgebis{\env{\Gamma}{\Theta}}{ D\{\inC{\cha^{\overline{p}}}{\til{x}}.P_2\}}{\type{ \ActS_2', \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2'}}}
%{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1}{ \INT'_2 }} & 
%  \infer
%{\judgebis{\env{\Gamma}{\Theta}}{\inC{\cha^{\overline{p}}}{\til{x}}.P_1 }{\type{\ActS_2, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2}}}
%{\judgebis{\env{\Gamma, \til{x}:\til{\capab}}{\Theta}}{P_2}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}}}
%\end{equation}
%with
%$$
% \jug_2 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST}}{ \INT_2}
%$$
%where Lemma~\ref{lem:context}  ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS \subseteq \ActS_1' \cup \ActS_2', \cha^p:!(\til{\capab}).{\ST}, \cha^{\overline{p}}:?(\til{\capab}).\overline{\ST} $, $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, and $ \INT \intpr \INT_1 \uplus \INT_2$.
%
%Now, by Lemma \ref{lem:substitution}(2)  we know $\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\til{c}}{\til{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{\INT_2}}$ with $\til{e} \downarrow \til{c}$. Moreover by Lemma \ref{l:ctxop}(3) and  rules \rulename{t:Par} and \rulename{t:Fill} we obtain the following type derivations:
%\begin{equation}\label{eq:output}
%\infer{\judgebis{\env{\Gamma}{ \Theta}}{C\{P_1\}}{\type{\ActS_1', \cha^p:\ST}{\INT_1'}}}
%{\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_1', \cha^p:\ST}{\INT_1'}} 
%&
%\judgebis{\env{\Gamma}{ \Theta}}{P_1}{\type{\ActS_1, \cha^p:\ST}{\INT_1}}}
%\end{equation}
%\begin{equation}\label{eq:input}
% \infer{\judgebis{\env{\Gamma}{\Theta}}{D\{P_2\sub{\til{c}\,}{\til{x}}\}}{\type{\ActS_2', \cha^{\overline{p}}:\overline{\ST}}{ \INT_2'}}}{
%\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS_2', \cha^{\overline{p}}:\overline{\ST}}{ \INT_2'}} 
%& \judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\til{c}\,}{\til{x}}}{\type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{ \INT_2}} }
%\end{equation}
%
% $$
%\infer{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}\big\} }{ \type{\ActS'}{\INT}}}
%{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS'}{\INT}}  
% & \infer
%{\judgebis{\env{\Gamma}{\Theta}}{C\{P_1\} \para  D\{P_2\sub{\til{c}\,}{\til{x}}\}}{\type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}\overline{\ST} }{ \INT_1' \addelta \INT_2'}}}
% {\eqref{eq:output}   & \eqref{eq:input}}
%}
%$$ 
%with
%$$
%\begin{array}{c}
% \jug_3 =  \Gamma; \Theta \vdash \type{\ActS_1, \cha^p:\ST}{\INT_1}\\
% \jug_4 =  \Gamma; \Theta \vdash \type{\ActS_2, \cha^{\overline{p}}:\overline{\ST}}{ \INT_2}\\
% \jug_5 =  \Gamma; \Theta \vdash \type{\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}\overline{\ST} }{ \INT_1' \addelta \INT_2'}
%\end{array}
%$$
%
%Since by inductive hypothesis  $\ActS_1'$ and $\ActS_2'$ are balanced, we infer that  $\ActS_1' \cup \ActS_2', \cha^p:\ST, \cha^{\overline{p}}:\overline{\ST}$ is balanced as well; this concludes the proof for this case.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\paragraph{\bf Case \rulename{r:Pass}} From Table~\ref{tab:semantics} we have:
%$$E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}\pired E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{\,q}}{x}\}\big\}$$
%
%By assumption we have  $\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}$, with $\ActS$ balanced. 
%By typing inversion on rules 
%%Using   Lemma \ref{lem:context} ($\Leftarrow$) and inversion on rules 
%\rulename{t:Fill},
%\rulename{t:Par}, \rulename{t:Cat}, and \rulename{t:Thr} we infer\done\todo[C19.]{We fixed a super index (was $\overline{p}$ should be $q$)}:
%$$
%\infer
%	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C\{\throw{\cha^{\,p}}{\cha_1^{\,q}}.P_1\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.P_2\}\big\}}{ \type{\ActS}{\INT}}}
%{\judgebis{\bullet_{\jug_0} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS}{\INT}} & \infer
%	{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{q}}.P_1\} \para  D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'}{\INT'}}}
%	{
%	\eqref{eq:throw}
%	&
%	\eqref{eq:catch}
%	}}
%$$
% with: 
% \begin{eqnarray}
% \ActS & = & \ActS_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST, \ActS_2, \cha^{\overline{p}}:?(\ST).\STT \\
% \ActS' & = & \ActS'_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST, \ActS'_2, , \cha^{\overline{p}}:?(\ST).\STT \\
% \jug_0 & = &  \Gamma; \Theta \vdash \type{\ActS'}{\INT'} \label{eq:srjugps2}
% \end{eqnarray}
% and, by Lemma~\ref{lem:context}, we infer $\ActS'_1 \subseteq \ActS_1$, $\ActS'_2 \subseteq \ActS_2$, and $\INT' \intpr \INT$.
% Moreover, \eqref{eq:throw}  corresponds to the subtree:
%\begin{equation}\label{eq:throw}
% \infer
%		{\judgebis{\env{\Gamma}{\Theta}}{C\{\throw{\cha^{p}}{\cha_1^{q}}.P_1\} }{ \type{\ActS'_1, \cha^p:!(\ST).\overline{\STT}, \cha_1^{q}:\ST}{ \INT'_1}}}
%		{\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT'_1 }}  & \infer
%{\judgebis{\env{\Gamma}{\Theta}}{\throw{\cha^p}{\cha_1^{q}}.P_1}{\type{\ActS''_1,\, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT''_1}}}
%{\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS''_1, \cha^p:\overline{\STT}}{ \INT''_1}} 
%		}}
%\end{equation}
%with $\ActS''_1 \subseteq \ActS'_1$ and $\INT''_1 \intpr \INT'_1$ (by Lemma~\ref{lem:context}) and
% \begin{eqnarray}
% \jug_1 & = &  \Gamma; \Theta \vdash \type{\ActS''_1,\, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{\INT''_1} \label{eq:srjugps3}
% \end{eqnarray}
%while \eqref{eq:catch}   corresponds to the subtree:
%\begin{equation}\label{eq:catch}
% \infer
%		{\judgebis{\env{\Gamma}{\Theta}}{ D\{\catch{\cha^{\overline{p}}}{x}.P_2\}}{ \type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2}}}
%		{\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2 }} & \infer
%{\judgebis{\env{\Gamma}{\Theta}}{\catch{\cha^{\overline{p}}}{x}.P_2 }{\type{\ActS''_2, \cha^{\overline{p}}:?(\ST).\STT}{\INT''_2}}}
%{\judgebis{\env{\Gamma}{\Theta}}{P_2}{\type{\ActS''_2, \cha^{\overline{p}}:\STT, x:\ST}{\INT''_2}}}	
%}
%\end{equation}
%with $\ActS''_2 \subseteq \ActS'_2$ and $\INT''_2 \intpr \INT'_2$ (by Lemma~\ref{lem:context}) and
% \begin{eqnarray}
% \jug_2 & = &  \Gamma; \Theta \vdash \type{\ActS''_2, \cha^{\overline{p}}:?(\ST).\STT}{\INT''_2} \label{eq:srjugps4}
% \end{eqnarray}
%%
%%and where by Lemma \ref{lem:context} ($\Leftarrow$) ensures $\ActS_1 \subseteq \ActS_1'$, $\ActS_2 \subseteq \ActS_2'$, $\ActS' \subseteq \ActS$ and $\ActS' = \ActS'_1 \cup \ActS'_2,  \cha^p:!(\ST).\overline{\STT}, \cha_1^q:\ST, \cha^{\overline{p}}:?(\ST).\STT$. Moreover we have $\INT_1 \intpr \INT_1'$, $\INT_2 \intpr \INT_2'$, $\INT' \intpr \INT$ and $\INT' = \INT'_1 \addelta \INT'_2$. Notice that as $\ActS$ is balanced, in $\ActS$ there is a $\cha_1^{\overline{q}}:\overline{\ST}$.
%
%We now describe how to obtain appropriately typed contexts $C^-$ and $D^+$, 
%based on the information already inferred  on contexts $C$ and $D$.
%We first consider the case of $C^-$. From \eqref{eq:throw}, we obtained 
%$$
%\judgebis{\bullet_{\jug_1} ; \env{\Gamma}{\Theta}}{C}{\type{\ActS'_1, \cha^p:!(\ST).\overline{\STT},\, \cha_1^{q}:\ST}{ \INT'_1 }}
%$$
%with $\jug_1$ as in \eqref{eq:srjugps3}. Then, using Lemma~\ref{l:ctxop}(2), we infer 
%$$
%\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^-}{\type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1 }}
%$$
%where 
% \begin{eqnarray}
% \jug_3 & = &  \Gamma; \Theta \vdash \type{\ActS''_1,\, \cha^p: \overline{\STT} }{\INT''_1}  \label{eq:srjugps5}
% \end{eqnarray}
%We may now reconstruct the derivation in~\eqref{eq:throw}, as follows:
%\begin{equation}\label{eq:passd}
%\infer
%		{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} }{ \type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1}}}
%		{\judgebis{\bullet_{\jug_3} ; \env{\Gamma}{\Theta}}{C^-}{\type{\ActS'_1, \cha^p:\overline{\STT}}{ \INT'_1 }} &\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS''_1, \cha^p:\overline{\STT}}{ \INT''_1}} 
%		}
%\end{equation}
%We now consider the case of $D^+$.
%By applying Lemma \ref{lem:substitution} \eqref{subchavar}
%on the premise concerning $P_2$ in \eqref{eq:catch}, we obtain
%$$\judgebis{\env{\Gamma}{ \Theta}}{P_2\sub{\cha_1^q}{x}}{\type{\ActS''_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT''_2}}$$ 
%From \eqref{eq:catch} we obtained
%$$
%\judgebis{\bullet_{\jug_2} ; \env{\Gamma}{\Theta}}{D}{\type{\ActS'_2, \cha^{\overline{p}}:?(\ST).\STT}{ \INT'_2 }}
%$$
%with $\jug_2$ as in \eqref{eq:srjugps4}. Then, using Lemma~\ref{l:ctxop}(1), we infer 
%$$
%\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2 }}
%$$
%where
% \begin{eqnarray}
% \jug_4 & = &  \Gamma; \Theta \vdash \type{\ActS''_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT''_2} \label{eq:srjugps6}
% \end{eqnarray}
%We can reconstruct the derivation depicted by \eqref{eq:catch}:
%%thus obtaining the following typing tree where we have used Lemma \ref{lem:context} ($\Rightarrow$) and rule \rulename{t:Par}, we also use the following subtree:
%\begin{equation}\label{eq:pass}
% \infer
%		{\judgebis{\env{\Gamma}{\Theta}}{ D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2}}}
%		{\judgebis{\bullet_{\jug_4} ; \env{\Gamma}{\Theta}}{D^+}{\type{\ActS'_2, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{ \INT'_2 }} & \judgebis{\env{\Gamma}{\Theta}}{P_2\sub{\cha_1^{q}}{x}}{\type{\ActS''_2, \cha^+:\STT, \cha_1^q:\ST}{\INT''_2}}	
%}
%\end{equation}
%Combining 
%\eqref{eq:passd} and \eqref{eq:pass}, 
%we may finally derive the type for the result of the reduction. Using rules \rulename{T:Par}  and \rulename{T:Fill} we obtain:
%$$
%\infer
%	{\judgebis{\env{\Gamma}{\Theta}}{E\big\{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}\big\}}{ \type{\ActS^*}{\INT}}}
%{\judgebis{\bullet_{\jug_5} ; \env{\Gamma}{\Theta}}{E}{\type{\ActS^*}{\INT}}
% & \infer
%	{\judgebis{\env{\Gamma}{\Theta}}{C^{-}\{P_1\} \para  D^{+}\{P_2\sub{\cha_1^{q}}{x}\}}{ \type{\ActS'_1 \cup \ActS'_2, \cha^p:\overline{\STT}, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT'}}}
%	{\eqref{eq:passd} & \eqref{eq:pass}
%	}}
%$$
%with
%$$
%\jug_5 =  \Gamma; \Theta \vdash \type{\ActS'_1 \cup \ActS'_2, \cha^p:\overline{\STT}, \cha^{\overline{p}}:\STT, \cha_1^q:\ST}{\INT'}
%$$
%Since by assumption $\ActS$ is balanced, we have that 
%by construction $\ActS^*$ is balanced as well. It is worth observing how contexts $C^{-}$ and $D^{+}$ correctly implement the fact that the number of active sessions is changed after delegating session $\kappa_1^{q}$ to process $P_2$.
% This concludes the proof for this case.
%
%
%% 
%\paragraph{\bf Cases \rulename{r:IfTr} and \rulename{r:IfFa}} Follows by an ease induction on the derivation tree.
%
%% 
%\paragraph{\bf Case \rulename{r:Close}} These follow by \done\todo[B38.]{Fixed, pls check}  the same reasoning as in  \rulename{r:Open} case.
%% 
%\paragraph{\bf Case \rulename{r:Branch}} This case is similar to  previous \rulename{r:I/O} case. 
%% 
%\paragraph{\bf Case \rulename{r:Str}} Follows from Theorem~\ref{th:congr} (Subject Congruence).
%% 
%\paragraph{\bf Case \rulename{r:Par}} Follows by induction and by applying rule $\rulename{t:Par}$.
%%
%\paragraph{\bf Case \rulename{r:Res}} Follows by induction and by the fact that  $\ActS$ is balanced. Indeed, by hypothesis and by inversion on rule \rulename{t:CRes} all the occurences of bracketed assignements ($[\cha^p:\ST]$) are necessarily balanced thus making it possible to apply the inductive hypothesis to the premise of the rule and concluding the analysis of this case and the proof of the theorem.
%% \end{description}
%\end{proof}

We are now ready to state our first main result:
 the \emph{absence of communication errors} for well-typed processes.
Recall that our notion of error process has been given in 
Definition~\ref{d:kred}.


\begin{theorem}[Typing Ensures Safety]\label{t:safety}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then $P$ never reduces into an error.
\end{theorem}

\begin{proof}
We assume, towards a contradiction, that there exists a $P_1$ 
such that ~$P \pired^* P_1$ and $P_1$ is an error process (as in~Def.~\ref{d:kred}).
By Theorem~\ref{th:subred} (Subject Reduction), $P_1$ is well-typed under a balanced typing $\D_1$.
Following Def.~\ref{d:kred}, there are two possibilities for $P_1$, namely 
it contains %(i)  exactly one $\kappa$-process, 
(i)~exactly two $\kappa$-processes which do not form a $\kappa$-redex and (ii)~three or more $\kappa$-processes.
Consider the second possibility.   
There are several combinations;
by inversion on rule \rulename{t:CRes}
we have that,
for some session types $\alpha_1$ and $\alpha_2$,
% either $\{\kappa^{p}: \alpha_1, \kappa^{\overline{p}}: \alpha_2\} \subseteq \D_1$ or  
$\{[\kappa^{p}: \alpha_1], [\kappa^{\overline{p}}: \alpha_2]\} \subseteq  \D_1$. 
In all cases, since the two $\kappa$-processes do not form a $\kappa$-redex then, necessarily, 
 $\alpha_1 \neq \overline{\alpha_2}$. This, however, contradicts the definition of balanced typings (Def.~\ref{d:balanced}).
The second possibility again contradicts Def.~\ref{d:balanced}, 
as in that case $\D_1$ would capture the fact that
at least one $\kappa$-process does not have a complementary partner for forming a $\kappa$-redex.
We thus conclude that well-typed processes never reduce to an error.
\end{proof}


\subsection{Session Consistency}\label{ss:consist}

We now investigate \emph{session consistency}: this is to 
%address a basic consequence of considering
enforce a basic discipline on 
the interplay of communicating behavior (i.e., session interactions) 
and evolvability behavior (i.e., update actions). 
Informally, %we say that a %session on channel $\kappa$ 
a process $P$
is called \emph{consistent} 
if %it is never disrupted by an evolvability step. 
%That is, 
whenever  %session on $\kappa$ is active and 
it has 
a $\kappa$-redex (cf. Def.~\ref{d:kred}) then 
possible interleaved update actions do not destroy such a redex.
%performing an update action does not affect the behavior of active sessions.

Below, we formalize this intuition. 
Let us write $P \pired_{\text{upd}} P'$ 
for any reduction inferred using rule $\rulename{r:Upd}$, possibly followed
by uses of rules $\rulename{r:Res}$, $\rulename{r:Str}$, and $\rulename{r:Par}$.
We then define:

%\begin{definition}[Session Consistency]\label{d:consist}
%Let $P$ be a process. 
%A session on channel $\kappa$ is \emph{consistent} in $P$ if,
%for all process $P', P''$ and contexts $E, C, D$ 
%such that 
%$$P \pired^{*} P' \equiv (\nu \til{\kappa})E\big\{C\{P_1\} \para  D\{P_2\}\big\}$$
%where $P_1$ and $P_2$ make $P'$ a $\kappa$-redex
%and $P' \pired_{\text{upd}} P''$, then there exist contexts $E', C'$, and $D'$ such that
%$$P'' \equiv (\nu \til{\kappa})E'\big\{C'\{P_1\} \para  D'\{P_2\}\big\}$$
%\end{definition}
%
%Hence, consistency on a session $\kappa$ %as formalized by Def.~\ref{d:consist} 
%says that update actions do not destroy $\kappa$-redexes. 
%Clearly, this definition does not rule out the possibility of interleaving intra-session communication 
%and update steps: it just requires update actions to reconfigure parts of the system not currently engaged into active sessions. 
%We find that giving priority to disciplined structured behavior over 
%runtime adaptation steps, as intended by this notion of consistency, 
%is a rather natural requirement.
%
%\jp{I feel consistency should be a property of processes, and focused on what the updates preserve
%rather than on what the sessions do. Hence I suggest stating consistency as:}

\begin{definition}[Consistency]\label{d:consis}
A process $P$ is \emph{update-consistent} 
if and only if,
 for all $P'$ and $\kappa$ 
such that $P \pired^{*} P'$ and $P'$ contains a $\kappa$-redex, 
if $P' \pired_{\text{upd}} P''$
then $P''$ contains a $\kappa$-redex.
\end{definition}

Recall that a \emph{located} $\kappa$-redex is a $\kappa$-redex in which one or both of
its constituting $\kappa$-processes are contained by least one located process.
This way, for instance, 
$$
\begin{array}{c}
\scomponent{l_2}{\,\scomponent{l_1}{\inC{\kappa^{\,p}}{\til{x}}.P_1}  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2\,} \\
\scomponent{l_1}{\inC{\kappa^{\,p}}{\til{x}}.P_1}  \para \scomponent{l_2}{\outC{\kappa^{\,\overline{p}}}{v}.P_2} \\
\scomponentbig{l_1}{\inC{\kappa^{\,p}}{\til{x}}.P_1  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2} 
\end{array}
$$
are located $\kappa$-redexes, whereas $\inC{\kappa^{\,p}}{\til{x}}.P_1  \para \outC{\kappa^{\,\overline{p}}}{v}.P_2$ is not.
From the point of view of consistency, the distinction between located and unlocated $\kappa$-redexes is relevant:
since update actions result from synchronizations on located processes, 
unlocated $\kappa$-redexes are always preserved by update actions, 
whereas located $\kappa$-redexes may be destroyed by a  update action.
We have the following auxiliary proposition.

\begin{proposition}\label{p:nonzero}
Let 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, with $\ActS$ balanced, 
be a well-typed process containing  
a $\kappa$-redex, for some $\kappa$. We have:
\begin{enumerate}[(a)]
\item $\ActS = \ActS', \kappa^p: \ST,  \kappa^{\overline{p}}:\overline{\ST}$
~~or~~ $\ActS = \ActS', [\kappa^p: \ST],  [\kappa^{\overline{p}}:\overline{\ST}]$
, for some session type $\ST$, and a balanced $\ActS'$.
\item If the $\kappa$-redex is located, then the runtime annotation for the location(s) hosting its 
constituting $\kappa$-processes is different from zero.
\end{enumerate}

\begin{proof}
Part~(a) is immediate from our definition of typing judgment, in particular from the fact that typing $\D$
records the types of currently active sessions, as implemented by channels such as $\kappa$.
Part~(b) follows directly by definition of typing rule \rulename{t:Loc} and part (a), observing that typing relies on the cardinality of $\D$
to compute (non zero) runtime annotations for locations. 
% and the fact that $\kappa$-redexes are essentially dual active sessions recorded in $\D$.
\end{proof}

\end{proposition}

\begin{theorem}[Typing Ensures Update Consistency]\label{t:consist}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$, with $\ActS$ balanced,
then $P$ is update consistent.
\end{theorem}

\begin{proof}
%By contradiction.
We assume, towards a contradiction, that there exist $P_1$, $P_2$, and $\kappa_1$ such that
(i)~$P\pired^*P_1$, (ii)~$P_1$ has a $\kappa_1$-redex,  (iii)~$P_1 \pired_{\text{upd}} P_2$, and 
(iv)~$P_2$ does not have a $\kappa_1$-redex.  Without loss of generality, 
we suppose that the reduction $P_1 \pired_{\text{upd}} P_2$ is due to a synchronization on location $l_1 \in \T$.
Since the $\kappa_1$-redex is destroyed by the update action from $P_1$ to $P_2$, the $\kappa_1$-redex in $P_1$ must necessarily be 
 a located $\kappa_1$-redex, i.e.,  in $P_1$, one or both $\kappa_1$-processes are contained inside $l_1$.
 Now, our reduction semantics (rule \rulename{r:Upd}) decrees that for such an update action to be enabled,
 the runtime annotation for $l_1$ in $P_1$ should be zero. However, by Theorem~\ref{th:subred} (Subject Reduction), we know that $P_1$ is well-typed under a balanced
 typing $\ActS_1$. Then, using well-typedness and Prop.~\ref{p:nonzero}(b)
we infer that the annotation for $l_1$ in $P_1$ must be different from zero: contradiction. 
Hence, update steps which destroy a  
$\kappa$-redex (located and unlocated) can never be enabled from a well-typed process 
  with a balanced typing (such as $P$) nor from any of its derivatives (such as $P_1$). We thus conclude that
  well-typedness implies update consistency.
\end{proof}

%\begin{proof}[Proof (Sketch)]
%Suppose $P$ reduces to a $P'$ 
%which contains a  $\kappa$-redex. 
%Subject reduction ensures that well-typedness under balanced typings is preserved by reduction.
%Therefore, $P'$ we have 
%$\judgebis{\env{\Gamma}{\Theta}}{P'}{\type{\ActS', \kappa^p: \ST, \kappa^{\overline{p}}:\overline{\ST}}{\INT'}}$
%for some $\ST, \INT'$
%and 
%balanced typing $\Delta'$. (The assignments could be bracketed, this is for simplicity.)
%Suppose further that a reduction $P'  \pired_{\text{upd}} P''$ is enabled.
%There are two cases.
%First, the update concerns a location which does not contain none of the $\kappa$-processes.
%That is, the update is external to this $\kappa$-redex.
%We observe that the reduction to $P''$ poses no danger for the $\kappa$-processes: 
%if the update is enabled then the runtime annotation for the location 
%to be updated must be 0. Recall this annotation is maintained by typing based on $\D$.
%In fact, this update preserves \emph{all} $\kappa$-redexes in $P'$.
%Second, the update concerns a location in which one or both $\kappa$-processes are contained.
%This case is not possible:
%because typing ensures that location annotations correspond to the number of open sessions at such a location, 
%since $\kappa$-processes are declared in $\D$ the annotation for the involved location is greater than 0 and so the update cannot be enabled, because of \rulename{r:Upd}.
%\end{proof}


%We can show that all sessions in our well-typed processes are consistent. 
%We can indeed state:
%
%\begin{corollary}[Con\-sist\-ency by Typing]\label{cor:cons}
%Suppose %\\%$P$ be a well-typed process. 
%$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} $
%is a well-typed process.
%Then every session $\ST_\qua \in \INT$ %that can be established along the evolution of $P$, we have that 
%is consistent, in the sense of Def.~\ref{d:consist}.
%\end{corollary}
%
%This result follows from Thm.~\ref{th:subred} 
%by observing that 
%enabling update actions only for 
%located processes without active sessions (cf. rule \rulename{r:Upd}), essentially 
%rules out the possibility of 
%updating a location containing 
%a communicating process $P_{\langle c \rangle}$, as defined above.
%Indeed, our type system ensures that the annotations enabling update actions 
%are correctly assigned and maintained along reduction.



